<!DOCTYPE html>
<html>
  <head>
    <meta charset='utf-8'>

    <link rel="stylesheet" type="text/css" 
      href="/assets/css/straybirds.css" media="screen" />
    <link rel="stylesheet" type="text/css" 
      href="/assets/css/pygments.css" media="screen" />

    <!-- MathJax Section Start -->

    <script type="text/javascript"
    src="http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML">
    </script>
    <script>
        MathJax.Hub.Config({
              tex2jax: {
              skipTags: ['script', 'noscript', 'style', 'textarea', 'pre']
              }
        });
        MathJax.Hub.Queue(function() {
            var all = MathJax.Hub.getAllJax(), i;
            for(i=0; i < all.length; i += 1) {
                all[i].SourceElement().parentNode.className += ' has-jax';
            }
        });
    </script>

    <!-- MathJax Section End -->

    <!-- Google Analytics Start-->
    <script>
  (function(i,s,o,g,r,a,m){i['GoogleAnalyticsObject']=r;i[r]=i[r]||function(){
  (i[r].q=i[r].q||[]).push(arguments)},i[r].l=1*new Date();a=s.createElement(o),
  m=s.getElementsByTagName(o)[0];a.async=1;a.src=g;m.parentNode.insertBefore(a,m)
  })(window,document,'script','//www.google-analytics.com/analytics.js','ga');

  ga('create', 'UA-48100787-1', 'minixalpha.github.io');
  ga('send', 'pageview');

</script>

    <!-- Google Analytics End -->

    <title>首页</title>
  </head>

  <body>
    <div class="container">
      <header>
        <div class="container">
          <h1>
              <a href="/" title="Home Page"> 潇湘夜雨 </a>
          <span class="github-src">
            <a href ="https://github.com/minixalpha/minixalpha.github.io"
               target="_blank"
               title="Fork me on GitHub">
              <img src="/assets/images/GitHub-Mark-Light-32px.png" alt="">
            </a>
          </span>
          </h1>
        </div>
      </header>

      <aside id="left-side">
        <h2> 分类 </h2>
  <ul class="category-list">
      
            
                <li>
                <a href="/categories/计算机系统"> 计算机系统 (3) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/java"> java (1) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/技术"> 技术 (5) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/工具"> 工具 (4) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/科研"> 科研 (5) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/生活"> 生活 (1) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/思想"> 思想 (2) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/c语言"> c语言 (4) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/虚拟机"> 虚拟机 (1) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/英语"> 英语 (8) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/读书"> 读书 (1) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/源代码阅读"> 源代码阅读 (10) </a>
                </li>
            
      
  </ul>

      </aside>

      <aside id="right-side">
        <h2> 归档 </h2>
  <ul class="archive-list">
    
    
    
        
        
        
        
            
            <li>
                <a href="/2014/05">
                    2014-05 (1)
                </a>
            </li>

        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
            
            <li>
                <a href="/2014/04">
                    2014-04 (3)
                </a>
            </li>

        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
            
            <li>
                <a href="/2014/03">
                    2014-03 (11)
                </a>
            </li>

        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
            
            <li>
                <a href="/2014/02">
                    2014-02 (6)
                </a>
            </li>

        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
            
            <li>
                <a href="/2014/01">
                    2014-01 (3)
                </a>
            </li>

        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
            
            <li>
                <a href="/2013/11">
                    2013-11 (10)
                </a>
            </li>

        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
            
            <li>
                <a href="/2013/10">
                    2013-10 (3)
                </a>
            </li>

        
        
    
  </ul>

      </aside>

      <article>

<ul class="post-list">
    
    <li>
      <div class="post-title">
        <a href="/%E8%8B%B1%E8%AF%AD/2014/03/23/learn-english-5.html"> 学习英语第五周</a> </br>
      </div>

      <div class="post-info">
        <ol>
          <li class="post-time">2014-03-23</li> 
          <li class="post-category"> 
           英语
          </li>
        </ol>
      </div>

      <div class="post-preview">
        <h1>学习英语第五周</h1>

<h2>阅读英文原著</h2>

<p>这周按照预定计划，把每天的阅读量降低了一半，每天20页左右。下面是时间表。</p>

<table><thead>
<tr>
<th align="center">Book</th>
<th align="center">Time</th>
<th align="center">Total Time</th>
<th align="center">Progress</th>
</tr>
</thead><tbody>
<tr>
<td align="center">Harry Potter and the Philosopher&#39;s Stone</td>
<td align="center">2014.03.17 12:45-14:15</td>
<td align="center">1.5h</td>
<td align="center">309/309</td>
</tr>
<tr>
<td align="center">Harry Potter and the Chamber Of Secrets</td>
<td align="center">2014.03.18 12:41-13:44</td>
<td align="center">1h</td>
<td align="center">41/341</td>
</tr>
<tr>
<td align="center">Harry Potter and the Chamber Of Secrets</td>
<td align="center">2014.03.19 12:26-13:04</td>
<td align="center">0.6h</td>
<td align="center">64/341</td>
</tr>
<tr>
<td align="center">Harry Potter and the Chamber Of Secrets</td>
<td align="center">2014.03.20 12:25-13:00</td>
<td align="center">35m</td>
<td align="center">86/341</td>
</tr>
<tr>
<td align="center">Harry Potter and the Chamber Of Secrets</td>
<td align="center">2014.03.23 20:53-21:22</td>
<td align="center">29m</td>
<td align="center">124/341</td>
</tr>
</tbody></table>
 
        <a href="/%E8%8B%B1%E8%AF%AD/2014/03/23/learn-english-5.html"> Read More ... </a> </br>
      </div>

    </li>
    
    <li>
      <div class="post-title">
        <a href="/%E8%8B%B1%E8%AF%AD/2014/03/16/learn-english-4.html"> 学习英语第四周</a> </br>
      </div>

      <div class="post-info">
        <ol>
          <li class="post-time">2014-03-16</li> 
          <li class="post-category"> 
           英语
          </li>
        </ol>
      </div>

      <div class="post-preview">
        <h1>学习英语第四周</h1>

<h2>阅读英文原著</h2>

<p>这周按照预定计划，把每天的阅读量降低了一半，每天20页左右。下面是时间表。</p>

<table><thead>
<tr>
<th align="center">Book</th>
<th align="center">Time</th>
<th align="center">Total Time</th>
<th align="center">Progress</th>
</tr>
</thead><tbody>
<tr>
<td align="center">Harry Potter and the Philosopher&#39;s Stone</td>
<td align="center">2014.03.10 12:30-13:30</td>
<td align="center">1h</td>
<td align="center">80/309</td>
</tr>
<tr>
<td align="center">Harry Potter and the Philosopher&#39;s Stone</td>
<td align="center">2014.03.11 12:30-13:30</td>
<td align="center">1h</td>
<td align="center">112/309</td>
</tr>
<tr>
<td align="center">Harry Potter and the Philosopher&#39;s Stone</td>
<td align="center">2014.03.12 12:40-13:40</td>
<td align="center">1h</td>
<td align="center">142/309</td>
</tr>
<tr>
<td align="center">Harry Potter and the Philosopher&#39;s Stone</td>
<td align="center">2014.03.13 12:45-13:45</td>
<td align="center">1h</td>
<td align="center">180/309</td>
</tr>
<tr>
<td align="center">Harry Potter and the Philosopher&#39;s Stone</td>
<td align="center">2014.03.14 12:36-13:14</td>
<td align="center">0.5h</td>
<td align="center">214/309</td>
</tr>
<tr>
<td align="center">Harry Potter and the Philosopher&#39;s Stone</td>
<td align="center">2014.03.15 14:43-15:05</td>
<td align="center">0.3h</td>
<td align="center">227/309</td>
</tr>
<tr>
<td align="center">Harry Potter and the Philosopher&#39;s Stone</td>
<td align="center">2014.03.13 13:39-14:45</td>
<td align="center">1h</td>
<td align="center">261/309</td>
</tr>
</tbody></table>
 
        <a href="/%E8%8B%B1%E8%AF%AD/2014/03/16/learn-english-4.html"> Read More ... </a> </br>
      </div>

    </li>
    
    <li>
      <div class="post-title">
        <a href="/%E7%A7%91%E7%A0%94/2014/03/14/mm-verify.html"> 内存模型的验证论文阅读</a> </br>
      </div>

      <div class="post-info">
        <ol>
          <li class="post-time">2014-03-14</li> 
          <li class="post-category"> 
           科研
          </li>
        </ol>
      </div>

      <div class="post-preview">
        <h1>内存模型的验证论文阅读</h1>

<h2>动态验证</h2>

<h3>Hangal2004</h3>

<ul>
<li><p>论文名
Hangal S, Vahia D, Manovit C, et al. TSOtool: A program for verifying memory systems using the memory consistency model[C]//ACM SIGARCH Computer Architecture News. IEEE Computer Society, 2004, 32(2): 114.</p></li>
<li><p>主要内容</p>

<ul>
<li>实现工具TSOtool，用于检测多处理器的共享内存系统</li>
<li>内存模型TSO</li>
<li>随机生成包含data race的程序</li>
<li>提出多项式时间算法，incomplete</li>
<li>检测出商业系统中的设计错误</li>
<li>根据内存模型定义一种次序关系，通过程序及结果构造有向图，
在图中找环</li>
<li>时间复杂度：最坏O(n^5)</li>
</ul></li>
<li><p>参考文献</p>

<ul>
<li>验证SC的复杂度, 将问题定义为VSC, VSC-read(map read to write), VSC-conflict(VSC-read + total order of write): Gibbons P B, Korach E. Testing shared memories[J]. SIAM Journal on Computing, 1997, 26(4): 1208-1244. </li>
</ul></li>
</ul>

<h3>Manovit 2005</h3>

<ul>
<li><p>论文名
Manovit C, Hangal S. Efficient algorithms for verifying memory consistency[C]//Proceedings of the seventeenth annual ACM symposium on Parallelism in algorithms and architectures. ACM, 2005: 245-252.</p></li>
<li><p>主要内容　</p>

<ul>
<li>将vector clock引入TSOtool工具</li>
<li>为VSC-conflict问题提出一个多项式算法</li>
<li>为VSC-read提出多项式算法，快速，有效，但不完备</li>
<li>时间复杂度：O(k*n^3)</li>
</ul></li>
<li><p>参考文献</p></li>
</ul>

<h3>Manovit 2006</h3>

<ul>
<li><p>论文名
Manovit C, Hangal S. Completely verifying memory consistency of test program executions[C]//High-Performance Computer Architecture, 2006. The Twelfth International Symposium on. IEEE, 2006: 166-175.</p></li>
<li><p>主要内容 </p>

<ul>
<li>在TSOtool中引入回溯，使验证TSO内存模型的算法完备</li>
<li>时间复杂度: O(p*n^3)</li>
</ul></li>
<li><p>参考文献</p></li>
</ul>
 
        <a href="/%E7%A7%91%E7%A0%94/2014/03/14/mm-verify.html"> Read More ... </a> </br>
      </div>

    </li>
    
    <li>
      <div class="post-title">
        <a href="/%E7%A7%91%E7%A0%94/2014/03/14/hd-mm.html"> 硬件内存模型论文阅读</a> </br>
      </div>

      <div class="post-info">
        <ol>
          <li class="post-time">2014-03-14</li> 
          <li class="post-category"> 
           科研
          </li>
        </ol>
      </div>

      <div class="post-preview">
        <h1>硬件内存模型论文阅读</h1>

<h2>引言</h2>

<p>内存模型定义了内存操作的语义,提出内存模型的目的在于指明内存操作之间的次序有何限制.</p>

<p>内存模型并不直接指定内存操作的次序,它只提供一种行为描述,只要<strong>你的执行结果</strong> 与 <strong>按内存模型规定的次序执行结果</strong> 一致就行,并不要求具体实现一定按这个顺序.</p>
 
        <a href="/%E7%A7%91%E7%A0%94/2014/03/14/hd-mm.html"> Read More ... </a> </br>
      </div>

    </li>
    
    <li>
      <div class="post-title">
        <a href="/%E7%A7%91%E7%A0%94/2014/03/12/jmm-papers.html"> Java 内存模型论文阅读</a> </br>
      </div>

      <div class="post-info">
        <ol>
          <li class="post-time">2014-03-12</li> 
          <li class="post-category"> 
           科研
          </li>
        </ol>
      </div>

      <div class="post-preview">
        <h1>Java 内存模型论文阅读</h1>

<h2>引言</h2>

<p>Java 的内存模型最早出现在1995年，但是自1997年起，这一内存模型被发现了许多严重的错误和缺陷，它阻碍了很多优化措施，对程序的安全性也没有足够的保证。2001年<a href="https://www.jcp.org/en/jsr/detail?id=133">JSR 133</a>被确立下来，由William Pugh领导，专家组的成员包括了Adve，Doug Lea， William Pugh等。2004年，JSR 133最终版本发布。2005年，Manson  Jeremy, William Pugh, 和 Sarita V. Adve 一同发表了论文 <em>The Java memory model</em>，描述了最新的Java内存模型，这一内存模型在Java 5.0中引入，一直沿用至今。此后，科学家们对Java内存模型进行了进一步的研究的探索，但大的改动并没有出现。</p>

<h2>论文介绍</h2>

<h3>Pugh2000</h3>

<ul>
<li><p>论文名
Pugh W. The Java memory model is fatally flawed[J]. Concurrency - Practice and Experience, 2000, 12(6): 445-455.</p></li>
<li><p>主要内容
介绍了现有Java内存模型的不足之处：
    * 难以理解，不同的人有不同解读
    * 禁止了很多编译器优化，大多数JVM实现都违反Java内存模型
    * 一些常用编程范式违反Java内存模型
    * 没有考虑到在共享内存，弱一致性内存模型下实现Java所带来的一些问题</p></li>
<li><p>参考文献</p>

<ul>
<li>Gontmakher 1997: 证明了Java内存模型需要Coherence</li>
</ul></li>
</ul>

<h3><strong>Manson 2005</strong></h3>

<ul>
<li><p>论文名
Manson J, Pugh W, Adve S V. The Java memory model[M]. ACM, 2005.</p></li>
<li><p>主要内容
JSR 133的成果，介绍了新的Java内存模型，由Java 5.0引入，沿用至今。
基本思想包括：
    * 对满足 Data Race Free 的程序保证顺序一致性(sequential consistency)
    * 对没有正确同步的程序，使用causality的概念加以限制，以保证程序的安全性
    * 新的内存模型足够强，以保证安全性，又足够弱，以保证编译器可以使用足够的优化</p></li>
<li><p>参考文献</p>

<ul>
<li>Lamport 1979: 提出 Sequential Consistency 概念</li>
<li>Relaxed models in academia and commercial hardware
        - Adve 1990
        - Adve 1993
        - Dubois 1986
        - Gharachorloo 1990
        - IBM 1983(System/370 Principles of Operation)
        - May 1994(The PowerPC Architecture)
        - Sites 1995(Alpha AXP Architecture Reference Manual)
        - Weaver 1994(The SPARC Architecture Manual)</li>
<li>SC for DRF
        - Adve 1990
        - Adve 1993
        - Gharachorloo 1990</li>
<li>Flaws in original Java Memory Model
        - Pugh 1999</li>
<li>Original Java Memory Model Research
        - Gosling 1996
        - Kotrajaras 2001
        - Saraswat 2004</li>
</ul></li>
</ul>

<h3><strong>Polyakov 2006</strong></h3>

<ul>
<li><p>论文名
Polyakov S, Schuster A. 
<em>Verification of the Java causality requirements</em>
[M]//Hardware and Software, Verification and Testing. Springer Berlin Heidelberg, 2006: 224-246.</p></li>
<li><p>主要内容
    * 证明验证causality是NP-complete的
    * 跟踪每个线程实际运行时 read 操作的顺序可以简化验证
    * 对可简化的验证提出了多项式算法
    * 不能简化的提出非多项式算法（仅用于短的测试序列）
    * 使用了Post-mortem的方法，实际运行一个多线程程序，在JVM或者定制过的JVM或者模拟器上运行程序，拿到trace，分析trace，以验证内存是否有问题
    * 使用frontier graph验证</p></li>
<li><p>参考文献</p>

<ul>
<li>Boehm 2005: 通过库实现多线程不能保证程序正确性</li>
<li>causal acyclicity 形式化定义(reach condition)：
      -   Suﬃcient System Requirements for  Supporting the PLpc Memory Model. 1993
      -  Specifying System Requirements for Memory Consistency Models. 1993</li>
<li>Gibbons 1993：使用frontier graph验证SC</li>
</ul></li>
</ul>
 
        <a href="/%E7%A7%91%E7%A0%94/2014/03/12/jmm-papers.html"> Read More ... </a> </br>
      </div>

    </li>
    
</ul>

<!-- Pagination links -->

<div class="pagination">
  
    <a href="/index.html">&laquo; Prev</a>
  

  
    
      <a href="/index.html">1</a>
    
  
    
      2
    
  
    
      <a href="/page3">3</a>
    
  
    
      <a href="/page4">4</a>
    
  
    
      <a href="/page5">5</a>
    
  
    
      <a href="/page6">6</a>
    
  
    
      <a href="/page7">7</a>
    
  
    
      <a href="/page8">8</a>
    
  

  
    <a href="/page3">Next &raquo;</a>
  
</div>



      </article>

      <div class="comments">
        
      </div>


      <footer>
        Copyright (c) minixalpha 2014
      </footer>

    </div>
  </body>
</html>
